Search for: All records

Battery-powered computing solutions have grown in importance and utility across a wide range of applications in the technology industry, including both consumer and industrial uses. Devices that are not attached to a stable and constant power source must ensure that all power consumption is minimized while necessary computation and communications are performed. WiFi networking is ubiquitous in modern devices, and thus the power consumption necessary to transmit data is of utmost concern for these battery powered devices. The Ad hoc OnDemand Distance Vector (AODV) routing algorithm is a widely adopted and adapted routing system for path finding in wireless networks. AODV’s original implementation did not include power consumption as a consideration for route determinations. The Energy Aware AODV (EA-AODV) algorithm was an attempt to account for energy conservation by varying broadcast power and choosing paths with distance between nodes as a consideration in routing. Lightning Strike AODV (LS-AODV) described in this paper is a proposed routing algorithm that further accounts for energy consumption in wireless networking by balancing energy in a network. Quality of service is maintained while energy levels are increased through networks using the LS-AODV algorithm. 

Incorporating symbolic reasoning into machine learning algorithms is a promising approach to improve performance on learning tasks that re- quire logical reasoning. We study the problem of generating a programmatic variant of referring expressions that we call referring relational pro- grams. In particular, given a symbolic representation of an image and a target object in that image, the goal is to generate a relational program that uniquely identifies the target object in terms of its attributes and its relations to other objects in the image. We propose a neurosymbolic program synthesis algorithm that combines a policy neural network with enumerative search to generate such relational programs. The policy neural net- work employs a program interpreter that provides immediate feedback on the consequences of the decisions made by the policy, and also takes into account the uncertainty in the symbolic representation of the image. We evaluate our algorithm on challenging benchmarks based on the CLEVR dataset, and demonstrate that our approach significantly outperforms several baselines. 

We propose trace abstraction modulo probability, a proof technique for verifying high-probability accuracy guarantees of probabilistic programs. Our proofs overapproximate the set of program traces using failure automata, finite-state automata that upper bound the probability of failing to satisfy a target specification. We automate proof construction by reducing probabilistic reasoning to logical reasoning: we use program synthesis methods to select axioms for sampling instructions, and then apply Craig interpolation to prove that traces fail the target specification with only a small probability. Our method handles programs with unknown inputs, parameterized distributions, infinite state spaces, and parameterized specifications. We evaluate our technique on a range of randomized algorithms drawn from the differential privacy literature and beyond. To our knowledge, our approach is the first to automatically establish accuracy properties of these algorithms.